COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDVAR X X0 X1 X2 Y Y0 Y1 Y2 Z Z0 Z1 Z2
C00004 ENDMK
C⊗;
DECLARE INDVAR X X0 X1 X2 Y Y0 Y1 Y2 Z Z0 Z1 Z2;
DECLARE INDVAR x x0 x1 x2 y y0 y1 y2 z z0 z1 z2 ε SEXP;
DECLARE INDVAR u u0 u1 u2 v v0 v1 v2 w w0 w1 w2 ε LIST;
DECLARE INDCONST nil ε LIST;

MOREGENERAL SEXP ≥ {LIST};

DECLARE OPCONST CONS 2;
DECLARE OPCONST CAR 1[R ← 600];
DECLARE OPCONST CDR 1[R ← 600];
DECLARE OPCONST cons(SEXP,SEXP) = SEXP;
DECLARE OPCONST car(SEXP) = SEXP[R←600];
DECLARE OPCONST cdr(SEXP) = SEXP[R←600];

DECLARE PREDCONST ATOM 1[R ← 500];
DECLARE PREDCONST atom(SEXP)[R←500];

AXIOM CONS:
	∀x y.(cons(x,y) = CONS(x,y))
;;

AXIOM CAR: ∀y.(car y = CAR y);;

AXIOM CDR: ∀y.(cdr y = CDR y);;

AXIOM ATOM: ∀x.(atom x ≡ ATOM x);;

AXIOM nil: atom nil;;

AXIOM LISP:
	∀x y.¬atom cons(x,y)
	∀x y.(car cons(x,y) = x)
	∀x y.(cdr cons(x,y) = y)
	∀y.(¬atom y ⊃ y = cons(car y,cdr y))
;;

AXIOM LIST: ∀x u.LIST(cons(x,u));;

DECLARE PREDPAR P 1;

AXIOM INDUCTION:
	P(nil) ∧ ∀u.(¬(u=nil) ∧ P(cdr u) ⊃ P(u)) ⊃ ∀u.P(u)
	∀x.(atom x ⊃ P(x)) ∧ ∀x.(¬atom x ∧ P(car x) ∧ P(cdr x) ⊃ P(x)) ⊃ ∀x.P(x)
;;